L:(Top List), n:, m:{0..(n+1)}. firstn(m;firstn(n;L)) ~ firstn(m;L) 

latex

Definitions	x:A. B(x), firstn(n;as), Y, t  T, {i..j}, if b then t else f fi , P  Q, tt, P  Q, , P & Q, P  Q, i  j < k, A  B, A, False, ff, T, True, SQType(T), , Unit, {T},
Lemmas	int seg wf, top wf, lt int wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert of lt int, le wf, le int wf, bnot wf, eqff to assert, bnot of lt int, assert of le int, squash wf, true wf